T. Litak, A. Visser; "Lewis meets Brouwer: constructive strict implication"
Tadeusz Litak
，
Albert Visser
https://arxiv.org/abs/1708.02143
直観主義様相論理
ではUnaryな
様相演算子
$ \Box
よりBinaryな
厳密含意
$ \to^\Box
を採用したほうが上手くやれる．ということが書いてあるらしい．